-- Missing Main
    DEF def(X:nat, Y:nat):nat == 0
